Inference at * 
Iof proof for Lemma select nth tl:


  T:Type, as:(T List), n:{0...||as||}, i:{0..(||as|| - n)}. nth_tl(n;as)[i] = as[(i+n)] 

latex

 by ((((CDToVarThen `as' ListInd) 
CollapseTHENM (Reduce 0))) 
CollapseTHENA (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 1. T : Type
C1: 2. T List
C1:   n:{0...0}, i:{0..(0 - n)}. nth_tl(n;[])[i] = [][(i+n)]
C2: 

C2: 1. T : Type
C2: 2. T List
C2: 3. u : T
C2: 4. v : T List
C2: 5. n:{0...||v||}, i:{0..(||v|| - n)}. nth_tl(n;v)[i] = v[(i+n)]
C2:   n:{0...||v||+1}, i:{0..((||v||+1) - n)}. nth_tl(n;[u / v])[i] = [u / v][(i+n)]
C.

Definitions	t  T, Y, ||as||, x:A. B(x)
Lemmas	int seg wf, int iseg wf